ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
↳ QTRS
↳ Overlay + Local Confluence
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(x, y), 0)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(x, y), 0)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(x, y), 0)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
Used ordering: Combined order from the following AFS and order.
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
trivial
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ EdgeDeletionProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x0)
ap(ap(ap(g, x0), x1), ap(s, x2))